es:ES, e:E. L:E List. (e':E. (e'  L)  e' c e) 

latex

Definitions

x. t(x), {T}, P  Q, P & Q, A c B, P  Q, e c e', P  Q, P  Q, x:A. B(x), x:A. B(x), , t  T, x(s), False, A, Dec(P)

Lemmas

member append, decidable l member, append wf, member singleton, cons member, es-causl-iff, or functionality wrt iff, iff functionality wrt iff, all functionality wrt iff, exists functionality wrt iff, decidable es-causle, decidable not, decidable cand, decidable es-E-equal, assert wf, not wf, event system wf, es-causl wf, es-pred-causl, es-pred wf, es-sender-causl, es-sender wf, es-isrcv wf, es-first wf, decidable assert, es-causle wf, l member wf, iff wf, es-E wf